es:ES, Fail:AbsInterface(Top).
fail-dcdr{i:l}(es;Fail)  e:EDec(e':E. ((e' <loc e) & ((e'  Fail)))) 

latex

Definitions	t  T, x:AB(x), P  Q, x:A. B(x), s = t, Dec(P), x:A  B(x), b, e  X, (e <loc e'), E, Type, x:A. B(x), P & Q, , decidable exists-fail, f(a), fail-dcdr{i:l}(es;Fail), a:A fp B(a), strong-subtype(A;B), ES, AbsInterface(A), Top
Lemmas	event system wf, top wf, es-interface wf, member wf, assert wf, es-locl wf, decidable wf, es-E wf